/FONT#0=BDR25/FONT#1=BDI25/FONT#2=NGR30/FONT#3=XMAS25/FONT#4=NGB25/FONT#5=NGR40
␈↓␈↓↓␈↓α␈↓β␈↓∧␈↓¬␈↓¬␈↓ βtARTIFICIAL INTELLIGENCE LABORATORY
␈↓ ∧"COMPUTER SCIENCE DEPARTMENT
␈↓ ¬	STANFORD UNIVERSITY
␈↓ ∧;STANFORD, CALIFORNIA 94305
␈↓
␈↓ ↓H

␈↓ ↓H

␈↓ ↓H

␈↓ ↓H

␈↓ ↓H

␈↓ ↓H
␈↓ α_␈↓ αh␈↓ β8␈↓ ∧λ␈↓ ∧X␈↓ ¬(␈↓ ¬xJune 18, 1974
␈↓ ↓H

␈↓ ↓H

␈↓ ↓H

␈↓ ↓H

␈↓ ↓H

␈↓ ↓H
Professor Garrett Birkhoff
␈↓ ↓H
Department of Mathematics
␈↓ ↓H
Harvard University
␈↓ ↓H
Science Center
␈↓ ↓H
One Oxford Street
␈↓ ↓H
Cambridge, Massachusetts 02138
␈↓ ↓H

␈↓ ↓H
Dear Garrett:
␈↓ ↓H

␈↓ ↓H
␈↓ α_Sorry␈αI␈αdidn't␈αget␈αaround␈αto␈αlooking␈αat␈αyour␈αarticle␈αuntil␈αnow,␈αand␈αI␈α
hope␈α
these␈α
comments␈α
are␈α
still␈α
of
␈↓ ↓Hsome␈α
use␈α
to␈α
you.

␈↓ α_In␈α
general,␈α
I␈α
shall␈α
leave␈α
artificial␈α
intelligence␈α
to␈α
Marvin␈α
Minsky␈α
even␈α
though␈α
his␈α
point␈α
of␈α
view␈α
and
␈↓ ↓Hmine␈αare␈αnot␈αquite␈αidentical.␈αEnclosed,␈αhowever,␈αis␈αa␈αreview␈αof␈αthe␈α␈↓↓Lighthill␈αReport␈↓␈αthat␈αwill␈αappear␈αin␈αthe
␈↓ ↓Hjournal␈α
␈↓↓Artificial␈α
Intelligence␈↓.␈α
Some␈α
of␈α
the␈α
ideas␈α
there␈α
expressed␈α
may␈α
be␈α
relevant␈α
to␈α
your␈α
purposes.

␈↓ α_From␈αmy␈αpoint␈αof␈αview,␈αthe␈αmain␈αomission␈αin␈αyour␈αarticle␈αis␈αany␈αdiscussion␈αof␈αthe␈αcomputer␈αprogram
␈↓ ↓Has␈α∀an␈α∀object␈α∀of␈α∀mathematical␈α∀study.␈α∀Since␈α∀the␈α∀properties␈α∪of␈α∪a␈α∪computer␈α∪program␈α∪are␈α∪mathematical
␈↓ ↓Hconsequences␈αof␈αits␈αstructure,␈αit␈αis␈αa␈αcontinuing␈αmathematical␈αdisgrace␈αthat␈αthe␈αbest␈αway␈αto␈αget␈αa␈αprogram
␈↓ ↓Hright␈α∂is␈α∂to␈α∂try␈α∂it␈α∂out␈α∂on␈α∂test␈α∂cases,␈α∂make␈α∂corrections␈α∂suggested␈α∂by␈α∂the␈α∂errors␈α∞found,␈α∞and␈α∞continue␈α∞this
␈↓ ↓Hprocess␈αuntil␈αyou␈αcan't␈αthink␈αof␈αany␈αmore␈αcases␈αto␈αtry.␈αThen␈αthe␈αnext␈αperson␈αwho␈αgets␈αthe␈αprogram␈αalmost
␈↓ ↓Himmediately␈α∂finds␈α∂additional␈α∂bugs.␈α∂Any␈α∂mathematician␈α∂should␈α∂want␈α∂to␈α∞prove␈α∞that␈α∞the␈α∞program␈α∞meets␈α∞its
␈↓ ↓Hspecifications.␈α
Moreover,␈α
the␈αnotion␈αof␈αformal␈αmathematical␈αproof␈αincludes␈αthe␈αproperty␈αthat␈αproofs␈αcan␈αbe
␈↓ ↓Hchecked␈α
by␈α
computer␈α
even␈α
if␈α
they␈α
can't␈α
easily␈α
be␈α
generated␈α
by␈α
computer.

␈↓ α_I␈α∂started␈α∂this␈α∂line␈α∂of␈α∂research␈α∂around␈α∂1960,␈α∂and␈α∂since␈α∂1965␈α∞it␈α∞has␈α∞become␈α∞increasingly␈α∞active,␈α∞and
␈↓ ↓Himportant␈αcontributions␈αhave␈αbeen␈αmade␈αby␈αRobert␈αFloyd,␈αDana␈αScott,␈αTony␈αHoare,␈αZohar␈αManna␈αand␈αmany
␈↓ ↓Hothers.␈α∪I␈α∪ccnsider␈α∪the␈α∪formalization␈α∪of␈α∪properties␈α∪of␈α∪computer␈α∪programs␈α∪and␈α∩their␈α∩proof␈α∩in␈α∩suitable
␈↓ ↓Haxiomatic␈α⊃systems␈α⊃to␈α⊃be␈α⊃the␈α⊃mathematical␈α⊃core␈α⊃of␈α⊃computer␈α⊃science.␈α⊂The␈α⊂properties␈α⊂considered␈α⊂include
␈↓ ↓Htermination,␈α
mathematical␈α
relations␈α
between␈α
input␈α
and␈α
output,␈α
equivalence␈αof␈αprograms,␈αthe␈αcorrectness␈αof
␈↓ ↓Hcompilers,␈α∂i.e.␈α∂that␈α∂the␈α∂object␈α∞program␈α∞carries␈α∞out␈α∞the␈α∞computation␈α∞described␈α∞by␈α∞the␈α∞source␈α∞program.␈α∞In
␈↓ ↓Hsupport␈α⊃of␈α⊃this␈α⊃goal␈α⊃proof␈α⊃checking␈α⊃programs␈α⊃have␈α⊃been␈α⊃written,␈α⊃axiomatizations␈α⊃of␈α⊃the␈α⊂properties␈α⊂of
␈↓ ↓Hprograms␈α
have␈α
been␈α
developed,␈α
and␈α
theorems␈α
have␈α
been␈α
proved␈α
that␈α
allow␈α
the␈α
correctness␈α
of␈α
a␈α
program␈α
to␈α
be
␈↓ ↓Hreduced␈α
to␈α
truth␈α
of␈α
a␈α
sentence␈α
in␈α
predicate␈α
calculus.

␈↓ α_In␈α⊂all␈α⊂this␈α⊂it␈α∂is␈α∂necessary␈α∂to␈α∂distinguish␈α∂the␈α∂␈↓↓theory␈α∂of␈α∂computation␈↓␈α∂in␈α∂which␈α∂the␈α∂correctness␈α∂of
␈↓ ↓Hparticular␈αprograms␈αis␈αstudied␈αfrom␈αthe␈α␈↓↓theory␈αof␈αcomputability␈↓␈αwhich␈αis␈αconcerned␈αwith␈αwhether␈αa␈αgiven
␈↓ ↓Hclass␈α
of␈α
problems␈α
can␈α
be␈α
solved␈α
at␈α
all␈α
by␈α
computer.

␈↓ α_Don␈αKnuth's␈αletter␈αgives␈αseveral␈αexamples␈αfrom␈αwhat␈αis␈αcalled␈α
applied␈α
complexity␈α
theory,␈α
i.e.␈α
a␈α
theory
␈↓ ↓Hthat␈α∩determines␈α∩upper␈α∩and␈α∩lower␈α∩bounds␈α∩to␈α⊃the␈α⊃amount␈α⊃of␈α⊃computation␈α⊃required␈α⊃to␈α⊃solve␈α⊃a␈α⊃problem.
␈↓ ↓HHowever,␈α⊂I␈α⊂think␈α⊂the␈α⊂subject␈α⊂deserves␈α⊂systematic␈α⊂recognition␈α⊂in␈α⊂any␈α⊂general␈α∂discussion␈α∂of␈α∂the␈α∂relations
␈↓ ↓Hbetween␈α
mathematics␈α
and␈α
computer␈α
science.

␈↓ α_I␈α
hope␈α
these␈α
remarks␈α
will␈α
be␈α
of␈α
some␈α
help.

␈↓ ↓H

␈↓ ↓H
␈↓ α_␈↓ αh␈↓ β8␈↓ ∧λ␈↓ ∧X␈↓ ¬(
␈↓ ↓H
␈↓ α_␈↓ αh␈↓ β8␈↓ ∧λ␈↓ ∧X␈↓ ¬(␈↓ ¬xSincerely yours,
␈↓ ↓H
␈↓ α_␈↓ αh␈↓ β8
␈↓ ↓H

␈↓ ↓H

␈↓ ↓H
␈↓ α_␈↓ αh␈↓ β8␈↓ ∧λ␈↓ ∧X␈↓ ¬(␈↓ ¬xJohn McCarthy
␈↓ ↓H
␈↓ α_␈↓ αh␈↓ β8␈↓ ∧λ␈↓ ∧X␈↓ ¬(␈↓ ¬xProfessor of Computer Science
␈↓ ↓H
␈↓ α_␈↓ αh␈↓ β8␈↓ ∧λ␈↓ ∧X␈↓ ¬(␈↓ ¬xDirector, Artificial Intelligence Laboratory
␈↓ ↓H